The present disclosure relates to satisfiability (SAT) solvers in general, and to utilizing formal methods in chip design and verification in particular.
One of the most challenging tasks in chip design is to reduce power consumption in electronic chip designs. Among the many techniques for power reduction, clock gating is one of the most known and widely used. Clock gating reduces the power consumption by partially disabling portions of the circuitry not required for the operation of the circuitry at a given cycle. A latch of a circuitry consumes power when it receives a clock signal, indicating a new cycle, and re-computes its value. Using clock gating technique, the clock signal to the latch is blocked when the recomputed value of the latch is not required in order for the circuitry to behave according to its designated purpose.
In order to provide for a clock gating function the chip design is inspected for clock gating opportunities. It is preferred that the clock gating function will not violate a timing constraint or consume more power than the power consumption reduced by gating the clock. The timing requirement may stipulate that the logic depth of the generated circuitry should not exceed some constant. To reduce the leakage overhead of a clock gating circuitry, latches with similar functions are grouped together and gated with a single function.
It will be noted that in the present application, latches refer to any form of state storage devices, such as for example flip-flops.